A:Type, eq:EqDecider(A), x, y:A, v:Top. x  dom(y : v)  x = y 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), Top, Prop, False, b, P  Q, false, eqof(d), p  q, P  Q, P  Q, P & Q, P  Q, x  dom(f), x : v
Lemmas	or functionality wrt iff, deq property, iff functionality wrt iff, assert of bor, bor wf, eqof wf, bfalse wf, assert wf, false wf, top wf, deq wf